package alloy.transform.atomize;

import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.BinaryFormula;
import alloy.ast.CompOp;
import alloy.ast.ElemFormula;
import alloy.ast.EmptyFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.Expr;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.LogicOp;
import alloy.ast.Node;

/**
 * Cleans up and canonicalizes conjoined formulas
 */
class CanonicalizeFormulasVisitor extends ASTDepthFirstReplacer {

	/**
	 * replaces none[A]->none[B] with none[A->B]
	 */
	public Object visit(BinaryExpr binExpr_) {
		visit((Node) binExpr_);

		if (binExpr_.getOp().equals(BinaryExprOp.RELATION)) {
			if (binExpr_.getLeft() instanceof EmptySetExpr
					&& binExpr_.getRight() instanceof EmptySetExpr) {

				Expr replacement = AtomizationVisitor.getNoneExpr(binExpr_
						.getType().toRelationType());
				return replacement;
			}

		}

		return binExpr_;
	}

	/**
	 * replaces "none[A] in anything" with true
	 */
	public Object visit(ElemFormula elemForm_) {
		visit((Node) elemForm_);

		if ((elemForm_.getOp().equals(CompOp.SUBSETCOLON) || elemForm_.getOp()
				.equals(CompOp.SUBSETIN))
				&& (elemForm_.getLeft() instanceof EmptySetExpr)) {
			Formula retForm = new EmptyFormula();
			retForm.setLocation(elemForm_.getLocation());
			return retForm;
		}

		return elemForm_;
	}

	public Object visit(BinaryFormula binForm_) {
		visit((Node) binForm_);
		Formula leftForm = binForm_.getLeft();
		Formula rightForm = binForm_.getRight();
		LogicOp op = binForm_.getOp();

		if (op.equals(LogicOp.AND)) {
			if (leftForm instanceof EmptyFormula) {

				if (rightForm instanceof EmptyFormula) {
					// both are empty

					// System.out.println("removed both left and right");
					Formula retForm = new EmptyFormula();
					retForm.setLocation(binForm_.getLocation());
					return retForm;
				} else {

					// System.out.println("removed left");
					return rightForm;
				}

			} else if (rightForm instanceof EmptyFormula) {

				// System.out.println("removed right");
				return leftForm;

			} else {

				return binForm_;
			}
		}

		return binForm_;
	}

	public Object visit(FormulaSeq formSeq_) {
		// should be handled by Formulas visitor
		visit((Node) formSeq_);

		Iterator formsIter = formSeq_.getFormulas().getFormulaIter();

		// check if the Formulas has no formulas--in that case this can be
		// reduced to empty
		if (!formsIter.hasNext()) {
			// no non-empty formulas exist in the original, return empty

			// System.out.println("removed FormulaSeq");
			Formula retForm = new EmptyFormula();
			retForm.setLocation(formSeq_.getLocation());
			return retForm;

		} else {
			Formula firstForm = (Formula) formsIter.next();

			// check if Formulas has only one formula--in this case you can
			// extract the formula.

			if (!formsIter.hasNext()) {
				// System.out.println("factored formula from FormulaSeq");
				return firstForm;
			}

		}

		return formSeq_;
	}

	/**
	 * Formulas do not implement Formula, so must return a Formulas object, even
	 * if empty.
	 */
	public Object visit(Formulas forms_) {
		visit((Node) forms_);

		List formulasToBeAdded = new LinkedList();

		Iterator formIter = forms_.getFormulaIter();
		boolean requiresChange = false;

		while (formIter.hasNext()) {
			Formula currentForm = (Formula) formIter.next();

			if (currentForm instanceof EmptyFormula) {
				requiresChange = true;
			} else {
				formulasToBeAdded.add(currentForm);
			}
		}

		if (requiresChange) {

			// System.out.println("simplified Formulas");

			// add the non empty formulas
			Formulas newForms = new Formulas(forms_.getLocation());

			for (Iterator newFormIter = formulasToBeAdded.iterator(); newFormIter
					.hasNext();) {
				Formula newForm = (Formula) newFormIter.next();
				newForms.addFormula(newForm);
			}

			return newForms;

		}

		return forms_;

	}

}
